The present application relates generally to an improved data processing apparatus and method and more specifically to mechanisms for performing optimal correlated array abstraction.
Contemporary hardware designs are often of substantial complexity, comprising a diversity of bit-level control logic, data paths, and performance-related artifacts including pipelining, multi-threading, out-of-order execution, and power-saving techniques. Memory arrays are ubiquitous in hardware designs, representing caches, main memory, lookup tables, and the like. Memory arrays may be used to either implement control logic or data paths.
Due to the complexity of hardware designs, verification, i.e. assessing that a design to be fabricated behaves as intended, performing equivalence checking to validate that two versions of a design (e.g., pre-synthesis and post-synthesis versions of a design) behave identically, and the like, is becoming an increasingly challenging and critical problem. Formal and semi-formal verification techniques are power tools for the construction of correct logic designs. These verification techniques have the power to expose even the most probabilistic uncommon scenario that may result in a functional design failure and ultimately have the power to prove that the design is correct, i.e. that no failing scenario exists. Unfortunately, formal verification techniques require computational resources which are exponential with respect to the size of the design under verification. Semi-formal verification techniques leverage formal algorithms to larger designs by applying them only in a resource-bounded manner, though at the expense of incomplete verification coverage.
The logic around the data flow in a design often contains the most subtle flaws. However, the data flow itself, including the arrays of state elements, e.g., memory arrays, often dominates the size of the design under verification. Because verification requires exponential resources with respect to design size, the data flow poses a tremendous bottleneck which often necessitates manual guidance of the verification process, e.g., to simplify or decompose the overall verification process, to expose these flaws and ultimately establish overall correctness of the design.
Various techniques to “abstract” a design under verification have been proposed. For example, the technique described in Baumgartner et al., U.S. Pat. No. 7,370,292, looks for gates within a design which are irrelevant to a verification problem and hence, may be replaced by non-deterministic values. The technique described in Bjesse, “Word-Level Sequential Memory Abstraction for Model Checking,” International Conference on Formal Methods in Computer-Aided Design, 2008, attempts to simplify arrays themselves by modeling a small number of “symbolic” rows to precisely capture write/read data consistency to the modeled rows, and non-deterministically resolving reads to unmodeled rows. In doing so, the technique of Bjesse effectively abstracts relative to “accesses” of the array, i.e. particular read operations which occur relative to a potential property failure.
Such abstractions may dramatically simplify the complexity of the overall verification problem in automatically reducing the size of the design under verification and eliminating the overhead of the data paths. However, such techniques have a substantial drawback in that they abstract arrays and array accesses independently from each other. This often entails a substantial penalty when attempting such abstraction on verification problems where arrays are correlated, a penalty that often leads to practical inapplicability of these techniques to designs having correlated arrays. Furthermore, such techniques tend to abstract arrays in an ad-hoc manner, without considering the impact of the chosen abstraction on subsequent verification complexity. This tends to be suboptimal, as when abstracting arrays, the particular chosen abstraction may have a substantial impact on how efficiently the resulting abstracted array may be represented for subsequent verification.